Introduction to Homotopy Type Theory